k:, A:((:( List)  (:  ( List))) List). Dec(y: List. q-sat-constraints(k;A;y)) 

latex

Definitions

t.1, t.2, q-constraints(k;A;y), ff, tt, if b then t else f fi , q-rel(r;x), True, T, P  Q, P  Q, r - s, P & Q, xL. P(x), {T}, False, A  B, A, P  Q, Dec(P), has-value(a), x. t(x), , P  Q, let x,y,z = a in t(x;y;z), A c B, x:A. B(x), t  T, q-sat-constraints(k;A;y), x:A. B(x), Unit, , (x  l), x(s), , , S  T

Lemmas

normalize-constraints-eq, qinverse q, pi1 wf, pi2 wf, mon ident q, qadd inv assoc q, qadd comm q, not functionality wrt iff, assert of bnot, eqff to assert, assert of eq int, eqtt to assert, iff transitivity, qadd preserves qless, qadd preserves qle, bnot wf, assert wf, bool wf, q-linear-sum, q-linear-times, true wf, squash wf, qmul wf, qadd wf, q-rel wf, member map, not wf, qless wf, qle wf, q-linear wf, eq int wf, ifthenelse wf, normalize-constraints wf, l member wf, l all wf2, length wf1, map wf, q-constraints wf, decidable wf, int inc rationals, select? wf, qsub wf, nat wf, rationals wf, decidable q-constraints-opt